﻿// ==++==
// 
//   Copyright (c) Microsoft Corporation.  All rights reserved.
// 
// ==--==

using System;
using System.Collections.Generic;
using System.Text;
using Microsoft.Pex.Graphs;
using Microsoft.Pex.Engine.ComponentModel;
using Microsoft.Pex.Engine.ExecutionNodes;
using Microsoft.Pex.Engine.Comprehensions;
using Microsoft.ExtendedReflection.Utilities.Safe.Diagnostics;
using Microsoft.ExtendedReflection.Interpretation;
using Microsoft.ExtendedReflection.Reasoning.ExecutionNodes;
using Microsoft.ExtendedReflection.ComponentModel;
using Microsoft.ExtendedReflection.Utilities.Safe;

namespace Microsoft.Pex.Fitness
{
    [__DoNotInstrument]
    public sealed class FitnessSearchGraphAttribute
        : SearchGraphAttribute
    {
        protected override SearchGraphBuilder CreateGraphBuilder(
            IPexExplorationComponent host,
            IVisualExecutionGraph visualExecutionGraph,
            IPexComprehensionManager comprehensionManager)
        {
            SafeDebug.AssumeNotNull(host, "host");
            SafeDebug.AssumeNotNull(visualExecutionGraph, "visualExecutionGraph");
            SafeDebug.AssumeNotNull(comprehensionManager, "comprehensionManager");

            IPexFitnessManager fitnessManager = ServiceProviderHelper.GetService<IPexFitnessManager>(host.Site);

            FitnessSearchGraphBuilder builder = new FitnessSearchGraphBuilder(
                this,
                host.ExplorationServices.TermManager,
                visualExecutionGraph,
                comprehensionManager,
                fitnessManager
                );
            return builder;
        }

        class FitnessSearchGraphBuilder :
            SearchGraphBuilder
        {
            readonly IPexFitnessManager fitnessManager;
            public FitnessSearchGraphBuilder(
                SearchGraphAttribute owner,
                TermManager termManager,
                IVisualExecutionGraph graph,
                IPexComprehensionManager comprehensionManager,
                IPexFitnessManager fitnessManager
                )
                :base(owner, termManager, graph, comprehensionManager)
            {
                SafeDebug.AssumeNotNull(fitnessManager, "fitnessManager");

                this.fitnessManager = fitnessManager;
            }

            protected override string UpdateLabel(IExecutionNode node, string label)
            {
                int fitness = this.fitnessManager.GetFitness(node);
                var result = SafeString.Format(
                    @"{0}
fit: {1}", label, fitness);

                return result;
            }
        }
    }
}
